{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 10.1 自然语言理解"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "第9章中描述的基于特征的文法形式可以很容易地从英语翻译到SQL。文法sql0.fcfg 说明如何将句子意思表示与句子分析串联组装。\n",
    "每个短语结构规则为特征SEM 构建值作补充。你可以看到这些补充非常简单；在每一种情况下，我们对分割的子成分用字符串连接\n",
    "操作+来组成父成分的值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "% start S\n",
      "S[SEM=(?np + WHERE + ?vp)] -> NP[SEM=?np] VP[SEM=?vp]\n",
      "VP[SEM=(?v + ?pp)] -> IV[SEM=?v] PP[SEM=?pp]\n",
      "VP[SEM=(?v + ?ap)] -> IV[SEM=?v] AP[SEM=?ap]\n",
      "NP[SEM=(?det + ?n)] -> Det[SEM=?det] N[SEM=?n]\n",
      "PP[SEM=(?p + ?np)] -> P[SEM=?p] NP[SEM=?np]\n",
      "AP[SEM=?pp] -> A[SEM=?a] PP[SEM=?pp]\n",
      "NP[SEM='Country=\"greece\"'] -> 'Greece'\n",
      "NP[SEM='Country=\"china\"'] -> 'China'\n",
      "Det[SEM='SELECT'] -> 'Which' | 'What'\n",
      "N[SEM='City FROM city_table'] -> 'cities'\n",
      "IV[SEM=''] -> 'are'\n",
      "A[SEM=''] -> 'located'\n",
      "P[SEM=''] -> 'in'\n"
     ]
    }
   ],
   "source": [
    "import nltk  \n",
    "nltk.data.show_cfg('grammars/book_grammars/sql0.fcfg')  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "这使我们能够分析SQL 查询"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "SELECT City FROM city_table WHERE Country=\"china\"\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "cp = load_parser('grammars/book_grammars/sql0.fcfg')\n",
    "query = 'What cities are located in China'\n",
    "trees = list(cp.parse(query.split()))\n",
    "answer = trees[0].label()['SEM']\n",
    "answer = [s for s in answer if s]\n",
    "q = ' '.join(answer)\n",
    "print(q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "最后，我们在数据库city.db 上执行查询，检索出一些结果"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "canton chungking dairen harbin kowloon mukden peking shanghai sian tientsin "
     ]
    }
   ],
   "source": [
    "from nltk.sem import chat80\n",
    "rows = chat80.sql_query('corpora/city_database/city.db', q)\n",
    "for r in rows: print(r[0], end=\" \")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "我们将重点探索NLTK 中的逻辑表示方式，所以将使用下列ASCII 版本的运算符："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "negation       \t-\n",
      "conjunction    \t&\n",
      "disjunction    \t|\n",
      "implication    \t->\n",
      "equivalence    \t<->\n"
     ]
    }
   ],
   "source": [
    "nltk.boolean_ops()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 的LogicParser()将逻辑表达式分析成表达式的各种子类："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<NegatedExpression -(P & Q)>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "read_expr('-(P & Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<AndExpression (P & Q)>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P & Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<OrExpression (P | (R -> Q))>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P | (R -> Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<IffExpression (P <-> --P)>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P <-> -- P')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 中的inference 模块通过一个第三方定理证明器Prover9 的接口，可以进行\n",
    "逻辑证明。推理机制的输入首先必须用LogicParser()分析成逻辑表达式。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-11-018378e4c881>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      4\u001b[0m \u001b[0mR\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mread_expr\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'SnF -> -FnS'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m      5\u001b[0m \u001b[0mprover\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mProver9\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m----> 6\u001b[1;33m \u001b[0mprover\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mprove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mNotFnS\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0mSnF\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mR\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mprove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m     37\u001b[0m         \u001b[1;33m:\u001b[0m\u001b[0mrtype\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mbool\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     38\u001b[0m         \"\"\"\n\u001b[1;32m---> 39\u001b[1;33m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mgoal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;36m0\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     40\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     41\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mabstractmethod\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_prove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    270\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    271\u001b[0m         stdout, returncode = self._call_prover9(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 272\u001b[1;33m                                                 verbose=verbose)\n\u001b[0m\u001b[0;32m    273\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    274\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_call_prover9\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    290\u001b[0m         \"\"\"\n\u001b[0;32m    291\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 292\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'prover9'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    293\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    294\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "lp = nltk.sem.Expression.fromstring\n",
    "SnF = read_expr('SnF')\n",
    "NotFnS = read_expr('-FnS')\n",
    "R = read_expr('SnF -> -FnS')\n",
    "prover = nltk.Prover9()\n",
    "prover.prove(NotFnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "一个命题逻辑的模型需要为每个可能的公式分配值True 或False。我们一\n",
    "步步的来做这个：首先，为每个命题符号分配一个值，然后确定布尔运算符的含义（即表1\n",
    "0-2）和运用它们到这些公式的组件的值，来计算复杂的公式的值。估值是从逻辑的基本符\n",
    "号映射到它们的值"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    " val = nltk.Valuation([('P', True), ('Q', True), ('R', False)])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "我们使用一个配对的链表初始化一个估值，每个配对由一个语义符号和一个语义值组\n",
    "成。所产生的对象基本上只是一个字典，映射逻辑符号（作为字符串处理）为适当的值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val['P']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "dom = set()\n",
    "g = nltk.Assignment(dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "让我们用val 初始化模型m："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "m = nltk.Model(dom, val)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "每一个模型都有一个evaluate()方法，可以确定逻辑表达式，如命题逻辑的公式，的\n",
    "语义值；当然，这些值取决于最初我们分配给命题符号如P、Q 和R 的真值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    " print(m.evaluate('(P & Q)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('-(P & Q)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('(P & R)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('(P | R)', g))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "逻辑表达式可以通过类型检查进行处理"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression angus>"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "expr = read_expr('walk(angus)', type_check=True)\n",
    "expr.argument"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.argument.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression walk>"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<e,?>"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "我们需要指定一个信号，作为一个字典来实施，明确的与非逻辑常量类型关联："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sig = {'walk': '<e, t>'} ##制定信号，将其作为字典实现与非逻辑常量类型之间的关联\n",
    "expr = read_expr('walk(angus)', signature=sig)\n",
    "expr.function.type"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 中的LogicParser 的parse()方法返回Expression 类的\n",
    "对象。这个类的每个实例expr 都有free()方法，返回一个在expr 中自由的变量的集合"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 中的LogicParser 的parse()方法返回Expression 类的\n",
    "对象。这个类的每个实例expr 都有free()方法，返回一个在expr 中自由的变量的集合。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('dog(cyril)').free()  #特指Cyril"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('x')}"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('dog(x)').free()   #自由变量x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('own(angus, cyril)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('exists x.dog(x)').free()  #封闭的"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('x')}"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('((some x. walk(x)) -> sing(x))').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('y')}"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('exists x.own(y, x)').free()   #自由变量y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "一阶定理证明"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-33-41161b338eaf>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      3\u001b[0m \u001b[0mR\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mread_expr\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'all x. all y. (north_of(x, y) -> -north_of(y, x))'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m      4\u001b[0m \u001b[0mprover\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mProver9\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m----> 5\u001b[1;33m \u001b[0mprover\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mprove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mNotFnS\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0mSnF\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mR\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mprove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m     37\u001b[0m         \u001b[1;33m:\u001b[0m\u001b[0mrtype\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mbool\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     38\u001b[0m         \"\"\"\n\u001b[1;32m---> 39\u001b[1;33m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mgoal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;36m0\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     40\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     41\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mabstractmethod\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_prove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    270\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    271\u001b[0m         stdout, returncode = self._call_prover9(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 272\u001b[1;33m                                                 verbose=verbose)\n\u001b[0m\u001b[0;32m    273\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    274\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_call_prover9\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    290\u001b[0m         \"\"\"\n\u001b[0;32m    291\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 292\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'prover9'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    293\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    294\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "NotFnS = read_expr('-north_of(f, s)') \n",
    "SnF = read_expr('north_of(s, f)')    \n",
    "R = read_expr('all x. all y. (north_of(x, y) -> -north_of(y, x))')  \n",
    "prover = nltk.Prover9()   \n",
    "prover.prove(NotFnS, [SnF, R]) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-34-b3d1d6ad6eca>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      1\u001b[0m \u001b[0mFnS\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mread_expr\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'north_of(f, s)'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m----> 2\u001b[1;33m \u001b[0mprover\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mprove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mFnS\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0mSnF\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mR\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mprove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m     37\u001b[0m         \u001b[1;33m:\u001b[0m\u001b[0mrtype\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mbool\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     38\u001b[0m         \"\"\"\n\u001b[1;32m---> 39\u001b[1;33m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prove\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mgoal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;36m0\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     40\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     41\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mabstractmethod\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_prove\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    270\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    271\u001b[0m         stdout, returncode = self._call_prover9(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 272\u001b[1;33m                                                 verbose=verbose)\n\u001b[0m\u001b[0;32m    273\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    274\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_call_prover9\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    290\u001b[0m         \"\"\"\n\u001b[0;32m    291\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 292\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_prover9_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'prover9'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    293\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    294\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the prover9 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on prover9, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "FnS = read_expr('north_of(f, s)')\n",
    "prover.prove(FnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 的语义关系可以用标准的集合论方法表示：作为元组的集合。例如：假设我们有\n",
    "一个域包括Bertie 、Olive 和Cyril，其中Bertie 是男孩，Olive 是女孩，而Cyril 是小狗。为了方便记述，我们用b、o 和c 作为模型中相应的标签。我们可以声明域如下：我们使用工具函数parse_valuation()将“符号=> 值”形式的字符串序列转换成一\n",
    "个Valuation 对象"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "dom=set(['b','o','c'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "v = \"\"\"\n",
    "bertie => b\n",
    "olive => o\n",
    "cyril => c\n",
    "boy => {b}\n",
    "girl => {o}\n",
    "dog => {c}\n",
    "walk => {o, c}\n",
    "see => {(b, o), (c, b), (o, c)}\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "val = nltk.Valuation.fromstring(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'bertie': 'b',\n",
      " 'boy': {('b',)},\n",
      " 'cyril': 'c',\n",
      " 'dog': {('c',)},\n",
      " 'girl': {('o',)},\n",
      " 'olive': 'o',\n",
      " 'see': {('c', 'b'), ('o', 'c'), ('b', 'o')},\n",
      " 'walk': {('c',), ('o',)}}\n"
     ]
    }
   ],
   "source": [
    "print(val)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('o', 'c') in val['see']"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "使用构造函数Assignment赋值。\n",
    "是一个从独立变量到域中实体的映射"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('b',) in val['boy']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "g = nltk.Assignment(dom,[('x','o'),('y','c')])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'x': 'o', 'y': 'c'}"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "使用print()查看赋值"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "g[c/y][o/x]\n"
     ]
    }
   ],
   "source": [
    "print (g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "为一阶逻辑公式估值"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [],
   "source": [
    "m = nltk.Model(dom,val)#创建一个模型"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(olive,y)',g)#调用evaluate（）方法计算真假"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'c'"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g['y']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(y,x)',g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "方法purge()从清除一个赋值中所有的绑定。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [],
   "source": [
    "g.purge()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{}"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Undefined'"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(olive,y)',g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "我们的模型已经包含了解释布尔运算的规则，任意复杂的公式都可以组合和评估"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(bertie,olive) & boy(bertie) & -walk(bertie)',g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " m.evaluate('exists x.(girl(x) & walk(x))', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('girl(x) & walk(x)', g.add('x', 'o'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 中提供了一个有用的工具：satisfiers()方法。它返回满足开放公式的所有个体\n",
    "的集合。该方法的参数是一个已分析的公式、一个变量和一个赋值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "fmla1 = read_expr('girl(x) | boy(x)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " m.satisfiers(fmla1, 'x', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'c', 'o'}"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla2 = read_expr('girl(x) -> walk(x)')\n",
    "m.satisfiers(fmla2, 'x', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla3 = read_expr('walk(x) -> girl(x)')\n",
    "m.satisfiers(fmla3, 'x', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('all x.(girl(x) -> walk(x))', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "为了检查这种歧义，我们对估值做如下修正"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "v2 = \"\"\"\n",
    "bruce => b\n",
    "cyril => c\n",
    "elspeth => e\n",
    "julia => j\n",
    "matthew => m\n",
    "person => {b, e, j, m}\n",
    "admire => {(j, b), (b, b), (m, e), (e, m), (c, a)}\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "val2 = nltk.Valuation.fromstring(v2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'admire': {('b', 'b'), ('c', 'a'), ('e', 'm'), ('j', 'b'), ('m', 'e')},\n",
       " 'bruce': 'b',\n",
       " 'cyril': 'c',\n",
       " 'elspeth': 'e',\n",
       " 'julia': 'j',\n",
       " 'matthew': 'm',\n",
       " 'person': {('b',), ('e',), ('j',), ('m',)}}"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "NLTK 中提供了一个有用的工具：satisfiers()方法。它返回满足开放公式\n",
    "的所有个体的集合。该方法的参数是一个已分析的公式、一个变量和一个赋值"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'a', 'b', 'c', 'e', 'j', 'm'}"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dom2 = val2.domain\n",
    "m2 = nltk.Model(dom2, val2)\n",
    "g2 = nltk.Assignment(dom2)\n",
    "fmla4 = read_expr('(person(x) -> exists y.(person(y) & admire(x, y)))')#a中的开放式一阶逻辑\n",
    "m2.satisfiers(fmla4, 'x', g2)#满足条件的所有x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'a', 'b', 'c', 'e', 'j', 'm'}"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dom2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla5 = read_expr('(person(y) & all x.(person(x) -> admire(x, y)))')#b中的一阶逻辑\n",
    "m2.satisfiers(fmla5, 'y', g2)#满足条件的所有x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b'}"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla6 = read_expr('(person(y) & all x.((x = bruce | x = julia) -> admire(x, y)))')\n",
    "m2.satisfiers(fmla6, 'y', g2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-60-bfa6727ff864>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      3\u001b[0m \u001b[0mc2\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mread_expr\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'-mortal(socrates)'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m      4\u001b[0m \u001b[0mmb\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mMace\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;36m5\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m----> 5\u001b[1;33m \u001b[0mprint\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0ma3\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mc1\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m     61\u001b[0m         \u001b[1;33m:\u001b[0m\u001b[0mrtype\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mbool\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     62\u001b[0m         \"\"\"\n\u001b[1;32m---> 63\u001b[1;33m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_build_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mgoal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;36m0\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     64\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     65\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mabstractmethod\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "a3 = read_expr('exists x.(man(x) & walks(x))')\n",
    "c1 = read_expr('mortal(socrates)')\n",
    "c2 = read_expr('-mortal(socrates)')\n",
    "mb = nltk.Mace(5)\n",
    "print(mb.build_model(None, [a3, c1]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-61-24dbe2429bd0>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mprint\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0ma3\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mc2\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m     61\u001b[0m         \u001b[1;33m:\u001b[0m\u001b[0mrtype\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mbool\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     62\u001b[0m         \"\"\"\n\u001b[1;32m---> 63\u001b[1;33m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_build_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mgoal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;36m0\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     64\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     65\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mabstractmethod\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "print(mb.build_model(None, [a3, c2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "print(mb.build_model(None, [c1, c2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-62-32ef9559d6ab>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      4\u001b[0m \u001b[0mg\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mread_expr\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'love(adam,eve)'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m      5\u001b[0m \u001b[0mmc\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mMaceCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0ma4\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0ma5\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0ma6\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m----> 6\u001b[1;33m \u001b[0mmc\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, verbose)\u001b[0m\n\u001b[0;32m    338\u001b[0m                     self._modelbuilder._build_model(self.goal(),\n\u001b[0;32m    339\u001b[0m                                                     \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0massumptions\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 340\u001b[1;33m                                                     verbose)\n\u001b[0m\u001b[0;32m    341\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    342\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "a4 = read_expr('exists y. (woman(y) & all x. (man(x) -> love(x,y)))')\n",
    "a5 = read_expr('man(adam)')\n",
    "a6 = read_expr('woman(eve)')\n",
    "g = read_expr('love(adam,eve)')\n",
    "mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6])\n",
    "mc.build_model()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "You have to call build_model() first to get a model!",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-63-7063bc6528ca>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mprint\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmc\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mvaluation\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36mvaluation\u001b[1;34m(mbc)\u001b[0m\n\u001b[0;32m     49\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     50\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mproperty\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 51\u001b[1;33m     \u001b[1;32mdef\u001b[0m \u001b[0mvaluation\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmbc\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m \u001b[1;32mreturn\u001b[0m \u001b[0mmbc\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'valuation'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     52\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     53\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_convert2val\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mvaluation_str\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mmodel\u001b[1;34m(self, format)\u001b[0m\n\u001b[0;32m    349\u001b[0m         \"\"\"\n\u001b[0;32m    350\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 351\u001b[1;33m             raise LookupError('You have to call build_model() first to '\n\u001b[0m\u001b[0;32m    352\u001b[0m                               'get a model!')\n\u001b[0;32m    353\u001b[0m         \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: You have to call build_model() first to get a model!"
     ]
    }
   ],
   "source": [
    "print(mc.valuation)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "You have to call build_model() first to get a model!",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-64-7063bc6528ca>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mprint\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmc\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mvaluation\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36mvaluation\u001b[1;34m(mbc)\u001b[0m\n\u001b[0;32m     49\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     50\u001b[0m     \u001b[1;33m@\u001b[0m\u001b[0mproperty\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 51\u001b[1;33m     \u001b[1;32mdef\u001b[0m \u001b[0mvaluation\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mmbc\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m \u001b[1;32mreturn\u001b[0m \u001b[0mmbc\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'valuation'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     52\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     53\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_convert2val\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mvaluation_str\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mmodel\u001b[1;34m(self, format)\u001b[0m\n\u001b[0;32m    349\u001b[0m         \"\"\"\n\u001b[0;32m    350\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 351\u001b[1;33m             raise LookupError('You have to call build_model() first to '\n\u001b[0m\u001b[0;32m    352\u001b[0m                               'get a model!')\n\u001b[0;32m    353\u001b[0m         \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: You have to call build_model() first to get a model!"
     ]
    }
   ],
   "source": [
    "print(mc.valuation)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<LambdaExpression \\x.(walk(x) & chew_gum(x))>"
      ]
     },
     "execution_count": 65,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "expr = read_expr(r'\\x.(walk(x) & chew_gum(x))')\n",
    "expr"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 66,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\x.(walk(x) & chew_gum(y))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x.(walk(x) & chew_gum(y))'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\x.(walk(x) & chew_gum(x))(gerald)\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\x.(walk(x) & chew_gum(x))(gerald)')\n",
    "print(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(walk(gerald) & chew_gum(gerald))\n"
     ]
    }
   ],
   "source": [
    "print(expr.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\y.(dog(cyril) & own(y,cyril))\n"
     ]
    }
   ],
   "source": [
    " print(read_expr(r'\\x.\\y.(dog(x) & own(y, x))(cyril)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(dog(cyril) & own(angus,cyril))\n"
     ]
    }
   ],
   "source": [
    " print(read_expr(r'\\x y.(dog(x) & own(y, x))(cyril, angus)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists x.P(x)\n"
     ]
    }
   ],
   "source": [
    "expr1 = read_expr('exists x.P(x)')\n",
    "print(expr1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists z.P(z)\n"
     ]
    }
   ],
   "source": [
    "expr2 = expr1.alpha_convert(nltk.sem.Variable('z'))\n",
    "print(expr2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 74,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr1 == expr2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "expr3 = read_expr('\\P.(exists x.P(x))(\\y.see(y, x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(\\P.exists x.P(x))(\\y.see(y,x))\n"
     ]
    }
   ],
   "source": [
    "print(expr3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists z1.see(z1,x)\n"
     ]
    }
   ],
   "source": [
    "print(expr3.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(\\X x.X(\\y.chase(x,y)))(\\P.exists x.(dog(x) & P(x)))\n"
     ]
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "tvp = read_expr(r'\\X x.X(\\y.chase(x,y))')\n",
    "np = read_expr(r'(\\P.exists x.(dog(x) & P(x)))')\n",
    "vp = nltk.sem.ApplicationExpression(tvp, np)\n",
    "print(vp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\x.exists z2.(dog(z2) & chase(x,z2))\n"
     ]
    }
   ],
   "source": [
    "print(vp.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all z4.(dog(z4) -> exists z3.(bone(z3) & give(angus,z3,z4)))\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "parser = load_parser('grammars/book_grammars/simple-sem.fcfg', trace=0)\n",
    "sentence = 'Angus gives a bone to every dog'\n",
    "tokens = sentence.split()\n",
    "for tree in parser.parse(tokens):\n",
    "     print(tree.label()['SEM'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 82,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(S[SEM=<walk(irene)>]\n",
      "  (NP[-LOC, NUM='sg', SEM=<\\P.P(irene)>]\n",
      "    (PropN[-LOC, NUM='sg', SEM=<\\P.P(irene)>] Irene))\n",
      "  (VP[NUM='sg', SEM=<\\x.walk(x)>]\n",
      "    (IV[NUM='sg', SEM=<\\x.walk(x)>, TNS='pres'] walks)))\n",
      "(S[SEM=<exists z5.(ankle(z5) & bite(cyril,z5))>]\n",
      "  (NP[-LOC, NUM='sg', SEM=<\\P.P(cyril)>]\n",
      "    (PropN[-LOC, NUM='sg', SEM=<\\P.P(cyril)>] Cyril))\n",
      "  (VP[NUM='sg', SEM=<\\x.exists z5.(ankle(z5) & bite(x,z5))>]\n",
      "    (TV[NUM='sg', SEM=<\\X x.X(\\y.bite(x,y))>, TNS='pres'] bites)\n",
      "    (NP[NUM='sg', SEM=<\\Q.exists x.(ankle(x) & Q(x))>]\n",
      "      (Det[NUM='sg', SEM=<\\P Q.exists x.(P(x) & Q(x))>] an)\n",
      "      (Nom[NUM='sg', SEM=<\\x.ankle(x)>]\n",
      "        (N[NUM='sg', SEM=<\\x.ankle(x)>] ankle)))))\n"
     ]
    }
   ],
   "source": [
    "sents = ['Irene walks', 'Cyril bites an ankle']\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "for results in nltk.interpret_sents(sents, grammar_file):\n",
    "    for (synrep, semrep) in results:\n",
    "        print(synrep)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 86,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all z8.(boy(z8) -> see(cyril,z8))\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "v = \"\"\"\n",
    " bertie => b\n",
    " olive => o\n",
    " cyril => c\n",
    " boy => {b}\n",
    " girl => {o}\n",
    " dog => {c}\n",
    " walk => {o, c}\n",
    " see => {(b, o), (c, b), (o, c)}\n",
    " \"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "g = nltk.Assignment(val.domain)\n",
    "m = nltk.Model(val.domain, val)\n",
    "sent = 'Cyril sees every boy'\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "results = nltk.evaluate_sents([sent], grammar_file, m, g)[0]\n",
    "for (syntree, semrep, value) in results:\n",
    "    print(semrep)\n",
    "    print(value)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "chase(z2,z3)\n"
     ]
    }
   ],
   "source": [
    "from nltk.sem import cooper_storage as cs\n",
    "sentence = 'every girl chases a dog'\n",
    "trees = cs.parse_with_bindops(sentence, grammar='grammars/book_grammars/storage.fcfg')\n",
    "semrep = trees[0].label()['SEM']\n",
    "cs_semrep = cs.CooperStore(semrep)\n",
    "print(cs_semrep.core)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 88,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "bo(\\P.all x.(girl(x) -> P(x)),z2)\n",
      "bo(\\P.exists x.(dog(x) & P(x)),z3)\n"
     ]
    }
   ],
   "source": [
    "for bo in cs_semrep.store:\n",
    "     print(bo)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 89,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Permutation 1\n",
      "   (\\P.all x.(girl(x) -> P(x)))(\\z2.chase(z2,z3))\n",
      "   (\\P.exists x.(dog(x) & P(x)))(\\z3.all x.(girl(x) -> chase(x,z3)))\n",
      "Permutation 2\n",
      "   (\\P.exists x.(dog(x) & P(x)))(\\z3.chase(z2,z3))\n",
      "   (\\P.all x.(girl(x) -> P(x)))(\\z2.exists x.(dog(x) & chase(z2,x)))\n"
     ]
    }
   ],
   "source": [
    "cs_semrep.s_retrieve(trace=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 90,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists x.(dog(x) & all z11.(girl(z11) -> chase(z11,x)))\n",
      "all x.(girl(x) -> exists z12.(dog(z12) & chase(x,z12)))\n"
     ]
    }
   ],
   "source": [
    "for reading in cs_semrep.readings:\n",
    "    print(reading)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "在NLTK 建立DRS 对象最简单的方法是通过解析一个字符串表示"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 91,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([x,y],[angus(x), dog(y), own(x,y)])\n"
     ]
    }
   ],
   "source": [
    "read_dexpr = nltk.sem.DrtExpression.fromstring\n",
    "drs1 = read_dexpr('([x, y], [angus(x), dog(y), own(x, y)])')\n",
    "print(drs1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 92,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "drs1.draw()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "每一个DRS 都可以转化为一阶逻辑公式，\n",
    "fol()方法实现这种转换"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 93,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists x y.(angus(x) & dog(y) & own(x,y))\n"
     ]
    }
   ],
   "source": [
    "print(drs1.fol())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "DRT 表达式有DRS连接运算符，用“+”符号表示\n",
    "自动进行α-转换绑定变量避免名称冲突"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 94,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(([x],[walk(x)]) + ([y],[run(y)]))\n"
     ]
    }
   ],
   "source": [
    "drs2 = read_dexpr('([x], [walk(x)]) + ([y], [run(y)])')\n",
    "print(drs2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 95,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([x,y],[walk(x), run(y)])\n"
     ]
    }
   ],
   "source": [
    "print(drs2.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 96,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "drs3 = read_dexpr('([], [(([x], [dog(x)]) -> ([y],[ankle(y), bite(x, y)]))])')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 97,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all x.(dog(x) -> exists y.(ankle(y) & bite(x,y)))\n"
     ]
    }
   ],
   "source": [
    "print(drs3.fol())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 98,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([u,x,y,z],[angus(x), dog(y), own(x,y), PRO(u), irene(z), bite(u,z)])\n"
     ]
    }
   ],
   "source": [
    "drs4 = read_dexpr('([x, y], [angus(x), dog(y), own(x, y)])')\n",
    "drs5 = read_dexpr('([u, z], [PRO(u), irene(z), bite(u, z)])')\n",
    "drs6 = drs4 + drs5\n",
    "print(drs6.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 99,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([u,x,y,z],[angus(x), dog(y), own(x,y), (u = [x,y,z]), irene(z), bite(u,z)])\n"
     ]
    }
   ],
   "source": [
    "print(drs6.simplify().resolve_anaphora())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 100,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([x,z15],[Angus(x), dog(z15), own(x,z15)])\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "parser = load_parser('grammars/book_grammars/drt.fcfg', logic_parser=nltk.sem.drt.DrtParser())\n",
    "trees = list(parser.parse('Angus owns a dog'.split()))\n",
    "print(trees[0].label()['SEM'].simplify())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "段落是一个句子的序列s1, ... sn，段落线是读法的序列s1-ri, ... sn-rj，每个序列\n",
    "对应段落中的一个句子。该模块按增量处理句子，当有歧义时保持追踪所有可能的线。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 101,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 102,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-102-3ea10d727ad3>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mdt\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mreadings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36mreadings\u001b[1;34m(self, sentence, threaded, verbose, filter, show_thread_readings)\u001b[0m\n\u001b[0;32m    351\u001b[0m         \"\"\"\n\u001b[0;32m    352\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_readings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 353\u001b[1;33m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_threads\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    354\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    355\u001b[0m         \u001b[1;31m# if we are filtering or showing thread readings, show threads\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_construct_threads\u001b[1;34m(self)\u001b[0m\n\u001b[0;32m    298\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_filtered_threads\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m{\u001b[0m\u001b[1;33m}\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    299\u001b[0m         \u001b[1;31m# keep the same ids, but only include threads which get models\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 300\u001b[1;33m         \u001b[0mconsistency_checked\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_check_consistency\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    301\u001b[0m         \u001b[1;32mfor\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mthread\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mitems\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    302\u001b[0m             \u001b[1;32mif\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mconsistency_checked\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_check_consistency\u001b[1;34m(self, threads, show, verbose)\u001b[0m\n\u001b[0;32m    393\u001b[0m                 \u001b[1;31m# if Mace4 finds a model, it always seems to find it quickly\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    394\u001b[0m                 \u001b[0mmb\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mMaceCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmax_models\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;36m20\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 395\u001b[1;33m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    396\u001b[0m             \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    397\u001b[0m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mFalse\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, verbose)\u001b[0m\n\u001b[0;32m    338\u001b[0m                     self._modelbuilder._build_model(self.goal(),\n\u001b[0;32m    339\u001b[0m                                                     \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0massumptions\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 340\u001b[1;33m                                                     verbose)\n\u001b[0m\u001b[0;32m    341\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    342\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 103,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-103-12ee84ab8479>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mdt\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0madd_sentence\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'No person dances'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mconsistchk\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36madd_sentence\u001b[1;34m(self, sentence, informchk, consistchk)\u001b[0m\n\u001b[0;32m    232\u001b[0m         \u001b[1;31m# of assumptions\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    233\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mconsistchk\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 234\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mreadings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    235\u001b[0m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mmodels\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mshow\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    236\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36mreadings\u001b[1;34m(self, sentence, threaded, verbose, filter, show_thread_readings)\u001b[0m\n\u001b[0;32m    351\u001b[0m         \"\"\"\n\u001b[0;32m    352\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_readings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 353\u001b[1;33m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_threads\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    354\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    355\u001b[0m         \u001b[1;31m# if we are filtering or showing thread readings, show threads\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_construct_threads\u001b[1;34m(self)\u001b[0m\n\u001b[0;32m    298\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_filtered_threads\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m{\u001b[0m\u001b[1;33m}\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    299\u001b[0m         \u001b[1;31m# keep the same ids, but only include threads which get models\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 300\u001b[1;33m         \u001b[0mconsistency_checked\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_check_consistency\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    301\u001b[0m         \u001b[1;32mfor\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mthread\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mitems\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    302\u001b[0m             \u001b[1;32mif\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mconsistency_checked\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_check_consistency\u001b[1;34m(self, threads, show, verbose)\u001b[0m\n\u001b[0;32m    393\u001b[0m                 \u001b[1;31m# if Mace4 finds a model, it always seems to find it quickly\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    394\u001b[0m                 \u001b[0mmb\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mMaceCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmax_models\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;36m20\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 395\u001b[1;33m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    396\u001b[0m             \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    397\u001b[0m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mFalse\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, verbose)\u001b[0m\n\u001b[0;32m    338\u001b[0m                     self._modelbuilder._build_model(self.goal(),\n\u001b[0;32m    339\u001b[0m                                                     \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0massumptions\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 340\u001b[1;33m                                                     verbose)\n\u001b[0m\u001b[0;32m    341\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    342\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "dt.add_sentence('No person dances', consistchk=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 104,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-104-f50a26a52c43>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mdt\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mretract_sentence\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'No person dances'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36mretract_sentence\u001b[1;34m(self, sentence, verbose)\u001b[0m\n\u001b[0;32m    251\u001b[0m             \u001b[1;32mreturn\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    252\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_sentences\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mdict\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m's%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[0mi\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0msent\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32mfor\u001b[0m \u001b[0mi\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0msent\u001b[0m \u001b[1;32min\u001b[0m \u001b[0menumerate\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_input\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 253\u001b[1;33m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mreadings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    254\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    255\u001b[0m             \u001b[0mprint\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Current sentences are \"\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36mreadings\u001b[1;34m(self, sentence, threaded, verbose, filter, show_thread_readings)\u001b[0m\n\u001b[0;32m    351\u001b[0m         \"\"\"\n\u001b[0;32m    352\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_readings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 353\u001b[1;33m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_threads\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    354\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    355\u001b[0m         \u001b[1;31m# if we are filtering or showing thread readings, show threads\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_construct_threads\u001b[1;34m(self)\u001b[0m\n\u001b[0;32m    298\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_filtered_threads\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m{\u001b[0m\u001b[1;33m}\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    299\u001b[0m         \u001b[1;31m# keep the same ids, but only include threads which get models\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 300\u001b[1;33m         \u001b[0mconsistency_checked\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_check_consistency\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    301\u001b[0m         \u001b[1;32mfor\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mthread\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mitems\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    302\u001b[0m             \u001b[1;32mif\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mconsistency_checked\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_check_consistency\u001b[1;34m(self, threads, show, verbose)\u001b[0m\n\u001b[0;32m    393\u001b[0m                 \u001b[1;31m# if Mace4 finds a model, it always seems to find it quickly\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    394\u001b[0m                 \u001b[0mmb\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mMaceCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmax_models\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;36m20\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 395\u001b[1;33m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    396\u001b[0m             \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    397\u001b[0m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mFalse\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, verbose)\u001b[0m\n\u001b[0;32m    338\u001b[0m                     self._modelbuilder._build_model(self.goal(),\n\u001b[0;32m    339\u001b[0m                                                     \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0massumptions\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 340\u001b[1;33m                                                     verbose)\n\u001b[0m\u001b[0;32m    341\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    342\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "dt.retract_sentence('No person dances', verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 105,
   "metadata": {},
   "outputs": [
    {
     "ename": "LookupError",
     "evalue": "\n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n===========================================================================",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mLookupError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-105-ea43f3560e6a>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mdt\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0madd_sentence\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'A person dances'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minformchk\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36madd_sentence\u001b[1;34m(self, sentence, informchk, consistchk)\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[1;31m# check whether the new sentence is informative (i.e. not entailed by the previous discourse)\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    218\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0minformchk\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 219\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mreadings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    220\u001b[0m             \u001b[1;32mfor\u001b[0m \u001b[0mtid\u001b[0m \u001b[1;32min\u001b[0m \u001b[0msorted\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    221\u001b[0m                 \u001b[0massumptions\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m[\u001b[0m\u001b[0mreading\u001b[0m \u001b[1;32mfor\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mrid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mreading\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mexpand_threads\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36mreadings\u001b[1;34m(self, sentence, threaded, verbose, filter, show_thread_readings)\u001b[0m\n\u001b[0;32m    351\u001b[0m         \"\"\"\n\u001b[0;32m    352\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_readings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 353\u001b[1;33m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_construct_threads\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    354\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    355\u001b[0m         \u001b[1;31m# if we are filtering or showing thread readings, show threads\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_construct_threads\u001b[1;34m(self)\u001b[0m\n\u001b[0;32m    298\u001b[0m         \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_filtered_threads\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m{\u001b[0m\u001b[1;33m}\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    299\u001b[0m         \u001b[1;31m# keep the same ids, but only include threads which get models\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 300\u001b[1;33m         \u001b[0mconsistency_checked\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_check_consistency\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    301\u001b[0m         \u001b[1;32mfor\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mthread\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_threads\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mitems\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    302\u001b[0m             \u001b[1;32mif\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mtid\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mconsistency_checked\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\discourse.py\u001b[0m in \u001b[0;36m_check_consistency\u001b[1;34m(self, threads, show, verbose)\u001b[0m\n\u001b[0;32m    393\u001b[0m                 \u001b[1;31m# if Mace4 finds a model, it always seems to find it quickly\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    394\u001b[0m                 \u001b[0mmb\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mMaceCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;32mNone\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0massumptions\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmax_models\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;36m20\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 395\u001b[1;33m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mmb\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mbuild_model\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    396\u001b[0m             \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    397\u001b[0m                 \u001b[0mmodelfound\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mFalse\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\api.py\u001b[0m in \u001b[0;36mbuild_model\u001b[1;34m(self, verbose)\u001b[0m\n\u001b[0;32m    338\u001b[0m                     self._modelbuilder._build_model(self.goal(),\n\u001b[0;32m    339\u001b[0m                                                     \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0massumptions\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 340\u001b[1;33m                                                     verbose)\n\u001b[0m\u001b[0;32m    341\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_result\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    342\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_build_model\u001b[1;34m(self, goal, assumptions, verbose)\u001b[0m\n\u001b[0;32m    200\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    201\u001b[0m         stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions),\n\u001b[1;32m--> 202\u001b[1;33m                                               verbose=verbose)\n\u001b[0m\u001b[0;32m    203\u001b[0m         \u001b[1;32mreturn\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mreturncode\u001b[0m \u001b[1;33m==\u001b[0m \u001b[1;36m0\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    204\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\mace.py\u001b[0m in \u001b[0;36m_call_mace4\u001b[1;34m(self, input_str, args, verbose)\u001b[0m\n\u001b[0;32m    213\u001b[0m         \"\"\"\n\u001b[0;32m    214\u001b[0m         \u001b[1;32mif\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;32mis\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 215\u001b[1;33m             \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_mace4_bin\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0m_find_binary\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'mace4'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    216\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    217\u001b[0m         \u001b[0mupdated_input_str\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m''\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\inference\\prover9.py\u001b[0m in \u001b[0;36m_find_binary\u001b[1;34m(self, name, verbose)\u001b[0m\n\u001b[0;32m    164\u001b[0m             \u001b[0murl\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;34m'http://www.cs.unm.edu/~mccune/prover9/'\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    165\u001b[0m             \u001b[0mbinary_names\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[0mname\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mname\u001b[0m \u001b[1;33m+\u001b[0m \u001b[1;34m'.exe'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 166\u001b[1;33m             verbose=verbose)\n\u001b[0m\u001b[0;32m    167\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    168\u001b[0m     \u001b[1;32mdef\u001b[0m \u001b[0m_call\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0minput_str\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mbinary\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0margs\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[1;33m=\u001b[0m\u001b[1;32mFalse\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    602\u001b[0m                 binary_names=None, url=None, verbose=False):\n\u001b[0;32m    603\u001b[0m     return next(find_binary_iter(name, path_to_bin, env_vars, searchpath,\n\u001b[1;32m--> 604\u001b[1;33m                                  binary_names, url, verbose))\n\u001b[0m\u001b[0;32m    605\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    606\u001b[0m def find_jar_iter(name_pattern, path_to_jar=None, env_vars=(),\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_binary_iter\u001b[1;34m(name, path_to_bin, env_vars, searchpath, binary_names, url, verbose)\u001b[0m\n\u001b[0;32m    596\u001b[0m     \"\"\"\n\u001b[0;32m    597\u001b[0m     for file in  find_file_iter(path_to_bin or name, env_vars, searchpath, binary_names,\n\u001b[1;32m--> 598\u001b[1;33m                      url, verbose):\n\u001b[0m\u001b[0;32m    599\u001b[0m         \u001b[1;32myield\u001b[0m \u001b[0mfile\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    600\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32mC:\\Users\\Public\\Anaconda3\\lib\\site-packages\\nltk\\__init__.py\u001b[0m in \u001b[0;36mfind_file_iter\u001b[1;34m(filename, env_vars, searchpath, file_names, url, verbose, finding_dir)\u001b[0m\n\u001b[0;32m    567\u001b[0m                         (filename, url))\n\u001b[0;32m    568\u001b[0m         \u001b[0mdiv\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;34m'='\u001b[0m\u001b[1;33m*\u001b[0m\u001b[1;36m75\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 569\u001b[1;33m         \u001b[1;32mraise\u001b[0m \u001b[0mLookupError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'\\n\\n%s\\n%s\\n%s'\u001b[0m \u001b[1;33m%\u001b[0m \u001b[1;33m(\u001b[0m\u001b[0mdiv\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mmsg\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mdiv\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m    570\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m    571\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mLookupError\u001b[0m: \n\n===========================================================================\nNLTK was unable to find the mace4 file!\nUse software specific configuration paramaters or set the PROVER9 environment variable.\n\n  Searched in:\n    - /usr/local/bin/prover9\n    - /usr/local/bin/prover9/bin\n    - /usr/local/bin\n    - /usr/bin\n    - /usr/local/prover9\n    - /usr/local/share/prover9\n\n  For more information on mace4, see:\n    <http://www.cs.unm.edu/~mccune/prover9/>\n==========================================================================="
     ]
    }
   ],
   "source": [
    "dt.add_sentence('A person dances', informchk=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "__init__() missing 1 required positional argument: 'parser_dirname'",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-109-9843072d8395>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[0;32m      7\u001b[0m       \u001b[1;33m(\u001b[0m\u001b[1;34m'^(He)$'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'PRP'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m      8\u001b[0m  ])\n\u001b[1;32m----> 9\u001b[1;33m \u001b[0mrc\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mDrtGlueReadingCommand\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mdepparser\u001b[0m\u001b[1;33m=\u001b[0m\u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mMaltParser\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mtagger\u001b[0m\u001b[1;33m=\u001b[0m\u001b[0mtagger\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     10\u001b[0m \u001b[0mdt\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mnltk\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mDiscourseTester\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m[\u001b[0m\u001b[1;34m'Every dog chases a boy'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'He runs'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0mrc\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     11\u001b[0m \u001b[0mdt\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mreadings\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mTypeError\u001b[0m: __init__() missing 1 required positional argument: 'parser_dirname'"
     ]
    }
   ],
   "source": [
    "from nltk.tag import RegexpTagger\n",
    "tagger = RegexpTagger(\n",
    "     [('^(chases|runs)$', 'VB'),\n",
    "      ('^(a)$', 'ex_quant'),\n",
    "      ('^(every)$', 'univ_quant'),\n",
    "      ('^(dog|boy)$', 'NN'),\n",
    "      ('^(He)$', 'PRP')\n",
    " ])\n",
    "rc = nltk.DrtGlueReadingCommand(depparser=nltk.MaltParser(tagger=tagger))\n",
    "dt = nltk.DiscourseTester(['Every dog chases a boy', 'He runs'], rc)\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "dt.readings(show_thread_readings=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "dt.readings(show_thread_readings=True, filter=True)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
